線形時相論理 (LTL)
linear temporal logic
時相演算子 (temporal operator)
next : $ Xp:=@_{1}p
globally : $ Gp:=\forall t@_tp
$ Gp=\bot R p,$ Gp=\neg F\neg p
安全性特性 : 惡い$ pは決して起こらない$ G\neg p
finally : $ Fp:=\exist t@_tp
$ Fp=\top Up.
活性特性 : 好い$ pが孰れ起きる$ Fp
until : $ pUq:=\exist t((\forall i_{i<t}@_ip)\land @_tq)
release : $ pRq:=@_tp\to\forall i_{i<t}@_iq
$ pRq=\neg(\neg pU\neg q).
Promela
truncated linear temporal logic (TLTL)